forall a: forall b:
forall Q:a->b:
forall R:a->b:
forall S:a->b:
(Q<S and R<S) => Q|R<S